R-base-ma(R)
== case R of 
== Rnone => 
== Rplus(left,right)=>rec1,rec2.
== Rinit(loc,T,x,V)=> case V of inl(v) => x : T initially x = t.v | inr(v) => x : T initially x = v
== Rframe(loc,T,x,L)=> only members of L affect x :T
== Rsframe(lnk,tag,L)=> only L sends on (lnk with tag)
== Reffect(loc,ds,knd,T,x,F)=> case F
== of inl(f) => with declarations 
== of inl(f) => ds:ds
== of inl(f) => da:knd : T
== of inl(f) => effect of knd(v) is x := s,v,t. f(s,v) s v
== o| inr(f) => with declarations 
== o| inr(f) => ds:ds
== o| inr(f) => da:knd : T
== o| inr(f) => effect of knd(v) is x := f s v
== Rsends(ds,knd,T,l,dt,g)=> with declarations 
== ds:ds
== da:knd : T  lnk-decl(l;dt)
== knd(v) sends g s v on link l
== Rpre(loc,ds,a,p,P)=> (precondition a:Outcome(p) is
== RP:State(ds) -> Bool)
== Rkframe(loc,k,L)=> k affects only members of L
== Rksframe(loc,k,L)=> k sends only on links in L
== Rrframe(loc,x,L)=> only members of L read x 

latex

---

clarification:

R-base-ma(R)
== case R of 
== Rnone => 
== Rplus(left,right)=>rec1,rec2.
== Rinit(loc,T,x,V)=> case V of inl(v) => x : T initially x = t.v | inr(v) => x : T initially x = v
== Rframe(loc,T,x,L)=> only members of L affect x :T
== Rsframe(lnk,tag,L)=> only L sends on (lnk with tag)
== Reffect(loc,ds,knd,T,x,F)=> case F
== of inl(f) => with declarations 
== of inl(f) => ds:ds
== of inl(f) => da:knd : T
== of inl(f) => effect of knd(v) is x := s,v,t. f(s,v) s v
== o| inr(f) => with declarations 
== o| inr(f) => ds:ds
== o| inr(f) => da:knd : T
== o| inr(f) => effect of knd(v) is x := f s v
== Rsends(ds,knd,T,l,dt,g)=> with declarations 
== ds:ds
== da:fpf-join(KindDeq;knd : T;lnk-decl(l;dt))
== knd(v) sends g s v on link l
== Rpre(loc,ds,a,p,P)=> (precondition a:Outcome(p) is
== RP:State(ds) -> Bool)
== Rkframe(loc,k,L)=> k affects only members of L
== Rksframe(loc,k,L)=> k sends only on links in L
== Rrframe(loc,x,L)=> only members of L read x 

latex

Definitions

es realizer ind, , x : t initially x = v, only members of L affect x :t, only L sends on (l with tg), case b of inl(x) => s(x) | inr(y) => t(y), x.A(x), f(a), with declarations ds:dsda:daeffect of k(v) is x := f s v, with declarations ds:dsda:dak(v) sends f s v on link l, f  g, KindDeq, x : v, lnk-decl(l;dt), (precondition a:Outcome(p) is P:State(ds) -> Bool), k affects only members of L, k sends only on links in L, only members of L read x

FDL editor aliases

R-base-ma